FDL - Nuprl Definition : prod-deq

Nuprl Definition : prod-deq

0,22

postcript pdf

prod-deq(A;B;a;b)
== (

A,B,a,b,p,q. q/q1,q2.
== (p/p1,p2.
== (b/eq,b1.
== (a/e1,a1.
== ((

%1.%1
== ((

%1.(<

%.<(

%1.%1(p1,q1)/%4,%5. %4((

%1.%1)((

%1.*)(*))))(a1)
== ((

%1.(<

%.,(

%1.%1(p2,q2)/%4,%5. %4((

%1.%1)((

%1.*)(*))))(b1)>
== ((

%1.(,

%.%/%1,%2. *>))
== (((

%1.%1/%2,%3. %3)
== ((((

%1.%1
== ((((

%1.(<p1,p2> = <q1,q2>
== ((((

%1.,<p1,p2> = <q1,q2>
== ((((

%1.,e1(p1,q1)

eq(p2,q2)
== ((((

%1.,e1(p1,q1) & eq(p2,q2)
== ((((

%1.,(

%1.%1)((

%1.<

%2.%2,

%2.%2>)(*))
== ((((

%1.,(

%1.%1)
== ((((

%1.,((

%1.%1(e1(p1,q1),eq(p2,q2)))
== ((((

%1.,((

p,q. Case q of
== ((((

%1.,((

p,q. inl(x)

Case p of
== ((((

%1.,((

p,q. inl(x)

inl(x)

%.<*,*>,

%.*>
== ((((

%1.,((

p,q. inl(x)

inr(y)

%.<any(%),*>,

%.%/%1,%2. any(%1)>
== ((((

%1.,((

p,q. inr(y)

Case p of
== ((((

%1.,((

p,q. inr(y)

inl(x)

%.<*,any(%)>,

%.%/%1,%2. any(%2)>
== ((((

%1.,((

p,q. inr(y)

inr(y)

%.<any(%),any(%)>,

%.%/%1,%2. any(%2)>))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(%5
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.((((%5((

%4.%4)((

%4.%4/%5,%6. %6((

%4.%4)((

%4.%4)(%3))))(%))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(%1)
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(%5
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((%6
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((((

%4.%4)((

%4.%4/%5,%6. %6((

%4.%4)((

%4.%4)(%3))))(%1))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(%)>
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(%6
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.((((%5((

%4.%4)((

%4.%4/%5,%6. %5((

%4.%4)((

%4.%4)(%3))))(%))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(%1)
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(%6
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((%6
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((((

%4.%4)((

%4.%4/%5,%6. %5((

%4.%4)((

%4.%4)(%3))))(%1))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(%)>>))))
== (A
== ,B
== ,a
== ,b)

latex

clarification:

prod-deq(A;B;a;b)
== (

A,B,a,b,p,q. q/q1,q2.
== (p/p1,p2.
== (b/eq,b1.
== (a/e1,a1.
== ((

%1.%1
== ((

%1.(<

%.<(

%1.%1(p1,q1)/%4,%5. %4((

%1.%1)((

%1.*)(*))))(a1)
== ((

%1.(<

%.,(

%1.%1(p2,q2)/%4,%5. %4((

%1.%1)((

%1.*)(*))))(b1)>
== ((

%1.(,

%.%/%1,%2. *>))
== (((

%1.%1/%2,%3. %3)
== ((((

%1.%1
== ((((

%1.(<p1,p2> = <q1,q2>

B
== ((((

%1.,<p1,p2> = <q1,q2>

B
== ((((

%1.,e1(p1,q1)

eq(p2,q2)
== ((((

%1.,e1(p1,q1) & eq(p2,q2)
== ((((

%1.,(

%1.%1)((

%1.<

%2.%2,

%2.%2>)(*))
== ((((

%1.,(

%1.%1)
== ((((

%1.,((

%1.%1(e1(p1,q1),eq(p2,q2)))
== ((((

%1.,((

p,q. Case q of
== ((((

%1.,((

p,q. inl(x)

Case p of
== ((((

%1.,((

p,q. inl(x)

inl(x)

%.<*,*>,

%.*>
== ((((

%1.,((

p,q. inl(x)

inr(y)

%.<any(%),*>,

%.%/%1,%2. any(%1)>
== ((((

%1.,((

p,q. inr(y)

Case p of
== ((((

%1.,((

p,q. inr(y)

inl(x)

%.<*,any(%)>,

%.%/%1,%2. any(%2)>
== ((((

%1.,((

p,q. inr(y)

inr(y)

%.<any(%),any(%)>,

%.%/%1,%2. any(%2)>))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(%5
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.((((%5((

%4.%4)((

%4.%4/%5,%6. %6((

%4.%4)((

%4.%4)(%3))))(%))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.<

%3.(%1)
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(%5
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((%6
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((((

%4.%4)((

%4.%4/%5,%6. %6((

%4.%4)((

%4.%4)(%3))))(%1))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. <

%2.,

%3.(%)>
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(%6
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.((((%5((

%4.%4)((

%4.%4/%5,%6. %5((

%4.%4)((

%4.%4)(%3))))(%))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.<

%3.(%1)
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(%6
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(((

%4.%4)
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((

%4.%4/%5,%6.
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((%6
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((((

%4.%4)((

%4.%4/%5,%6. %5((

%4.%4)((

%4.%4)(%3))))(%1))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.((((%2))))
== ((((

P1,P2,Q1,Q2,%,%1. ,

%2.,

%3.(%)>>))))
== (A
== ,B
== ,a
== ,b)

latex

Definitions b, P & Q, p q, prod-deq(A;B;a;b)

FDL editor aliases prod-deq

origin

Definitions	b, P & Q, p q, prod-deq(A;B;a;b)
FDL editor aliases	prod-deq